\section{Result}
\subsection{Implemented Features}
The list of implemented features is as follows.
\begin{itemize}
\item {
    \emph{Deadlock detection}: It often happens that a state is reached from where it is not possible to solve the puzzle. Usually this is because a block can not be moved or because a block can no longer reach the goal it was meant to have. We call these states deadlock states. By definition every next state that can be reached is also a deadlock state, we have written algorithms to detect these states. They have significantly reduced the statespace and improved the speed of our model checker.

We have implemented several deadlock detection algorithms. These have been used to generate BDD's with all the possible states that are not deadlocks. We applied this non-deadlock BDD to our relation function (with the \emph{and} operator). As a result, our relation function now only calculates next states which are not deadlock states. We have a lot of time on implementing deadlock detection in contrast to other features, because we want to solve large puzzles. We detect the following deadlocks.
    \begin{enumerate}
    \item {
        Positions marked \emph{x} may never have blocks, because it is not possible to move these blocks to a goal anymore.
        We calculate these positions by starting from the goal positions, and checking from where the man could have pushed these blocks. All tiles from where it is not possible to push a block to any goal are deadlock positions. \\
        Implemented in Solver.getNonDeadLockBlockPositions().
        \begin{lstlisting}[basicstyle=\ttfamily]
	       #####
	       #xxx#
	       #$$$#
	    ####   #
	    #x  .#$##
	    #x$.$. .#
	    #xx#.#.##
	    ########
        \end{lstlisting}
    }
    \item {
        Simple bipartite deadlocks; For every goal we calculate from which positions it is possible to push a block into that goal. In all these positions (including the goal itself) there must be at least one block. If this is not the case, then the game is in a deadlock state.

For the right goal, there must be a block either on the goal or on the position marked \emph{x}.\\
        Implemented in Solver.getSimpleNonBiparitieDeadlockPositions().
        \begin{lstlisting}[basicstyle=\ttfamily]
	    ######
	    #.$ @#
	    ## x.#
	     #   #
	     #####
        \end{lstlisting}
    }
    \item {
        Dead corridor situation; a man must not push a block in a corridor where there is no goal.\\
        Implemented in Solver.getNonDeadCorridorStates().
        \begin{lstlisting}[basicstyle=\ttfamily]
            ####
        #####. #
        #DDDD  # D = dead end squares which are deadlock squares  
        #####$ # 
            #@ #
            ####
        \end{lstlisting}
    }
    \item {
        The four block square situation. In this situation the four blocks block each other's movement\\
        Implemented in Solver.getNotImmovableBlocksStates().
        \begin{lstlisting}[basicstyle=\ttfamily]
        $$
        $$
        \end{lstlisting}
    }
    \item {
        The three block and wall square situation. \\
        Implemented in Solver.getNotImmovableBlocksStates().
        \begin{lstlisting}[basicstyle=\ttfamily]
        $# or #$ or $$ or $$
        $$    $$    #$    $#
        \end{lstlisting}
    }
    \item {
        The two block and two wall square situation. \\
        Implemented in Solver.getNotImmovableBlocksStates().
        \begin{lstlisting}[basicstyle=\ttfamily]
        ## or #$ or $$ or $#
        $$    #$    ##    $#
        \end{lstlisting}
    }
    \item {
        The two block and two wall tetris block situation. This situation is like the previous situations
         but the walls are in different positions in relation to the blocks\\
        Implemented in Solver.getNotImmovableBlocksStates().
        \begin{lstlisting}[basicstyle=\ttfamily]
        #$  or #$  or #  or  #
         $#     $#    $$    $$
                       #    #
        \end{lstlisting}
    }
    \end {enumerate}
To test the difference the deadlock states make use the -nodeadlockremoval switch.
}
\item {
\emph{Computing the (shortest) trace to an unsolvable state}: Using our algorithms for detecting deadlocks, we have implemented a function to get the trace to the first deadlock state. This is done in the same way as our normal algorithm, but instead of checking if we have reached a goal state, we check if a deadlock state has been reached. It should be noted that even though we have thought about deadlocks for quite a while, we do not detect every complex deadlock state. In all cases that we tested we believed that the resulting trace was the shortest. This is probably because more complex deadlocks that we can not detect require more steps than the deadlocks that we do detect. Still, it is possible that this method does not find the shortest trace.

To compute the shortest trace to a deadlock state use the -d switch.
}
\item {
\emph{Compute and count the set of all reachable states that have a solution}: We have implemented a feature to make our solve function continue till the statespace has reached the greatest fixpoint. It will then print the number of reachable states that have a solution.

To use this feature, use the -countsolutions switch.
}
\item {
\emph{Check if a certain lurd-string is still solvable}: It is possible to supply a lurd sting as an argument to our solver. The transitions in the lurd string will be applied to the initial state. If the string leads to an invalid state (the man walking of the board) or a deadlock state (only those which our deadlock detection algorithms detect) it will be reported. Else our solver will return the solution from the state that results from applying the lurd string.

To use this feature, use the -lurd switch followed by a lurdstring
}
\end{itemize}

\subsection{Capabilities \& Performance Indication}
We tested the capabilities of our model checker on an Intel Core 2 Duo (E8400) @ 4.0 GHz with 4GB of ram.
We initialize the JVM with arguments -Xms3500m -Xmx3501m which should result in a heap size of about 3500 Mb.
In Solver.init() we configured to nodesize to be 20000000 and the cachesize to be 2000000. We use the native Java BDD implementation in JavaBDD.
The results we got were as follows. Note this is not a good quality benchmark, but only an indication of the solver's performance.
The number of states are the amount of states until a solution is found with the deadlock states excluded.
\begin{center}
	\begin{tabular}{lll}
		\textbf{Screen} & \textbf{\#states} & \textbf{time (ms)} \\ \hline
		107 & 2057 & 1500 \\
		1001 & 11790 & 2131 \\
		387 & 95395 & 3468 \\
		372 & 322400 & 5142 \\
		792 & 806144 & 11160 \\
		747 & 1154531 & 9397 \\
		38 & & \\
	\end{tabular}
\end{center}

In order to improve the model checker's performance we added deadlock detection and a particular order of variables.
